es:ES, p:(E(E + Top)). causal-predecessor(es;p)  SWellFounded(p-graph(E;p)(y,x)) 

latex

Definitions	suptype(S; T), S  T, A c B, Top, x f y, p-graph(A;f), R1 => R2, , x,y. t(x;y), t  T, P  Q, x:A. B(x), causal-predecessor(es;p), x(s1,s2)
Lemmas	es-causl-swellfnd, do-apply wf, can-apply wf, assert wf, event system wf, top wf, es-E wf, causal-predecessor wf, p-graph wf2, es-causl wf, strongwf-monotone